[ add ] injectivity of suc for relation m ≡ n (mod o) for {{NonZero o}}#2971
[ add ] injectivity of suc for relation m ≡ n (mod o) for {{NonZero o}}#2971jamesmckinna wants to merge 14 commits intoagda:masterfrom
suc for relation m ≡ n (mod o) for {{NonZero o}}#2971Conversation
|
Last commit tidies up notations etc. |
Can now: by generalising |
src/Data/Nat/DivMod.agda
Outdated
| ≡[o]%⇒≅%[o] {x = m} {y = n} eq with ≤-total m n | ||
| ... | inj₁ m≤n = fwd (≡[o]%⇒≲%[o] eq m≤n) | ||
| ... | inj₂ n≤m = bwd (≡[o]%⇒≲%[o] (sym eq) n≤m) |
There was a problem hiding this comment.
This proof could be refactored in terms of Relation.Binary.Consequences.wlog, but my first attempt ended up more verbose and harder to read than this version. But perhaps eventually that combinator will be reimplemented, and with it, a suitable refactoring of this lemma.
There was a problem hiding this comment.
Notwithstanding that wlog can be used, I think the above proof is easier to read.
There was a problem hiding this comment.
And now, in terms of Sum elimination, so avoiding the appeal to with.
|
@JacquesCarette hope I've addressed all your feedback |
jamesmckinna
changed the title
m ≡ n (mod o) for {{NonZero o}}suc for relation m ≡ n (mod o) for {{NonZero o}}
4 participants
Taken from the discussion at https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/suc.20injective.20under.20_.25_/with/582024092 :
m ≲%[ o ] n = ∃ λ k → n ≡ m + k * om % o ≡ n % oin terms of (the symmetric closure of)m ≲%[ o ] n(suc m) % o ≡ (suc n) % o → m % o ≡ n % oSymClosurePossible TODO:
_≲%[ o ]_satisfiesIsPreorder _≡_, indeedIsPartialOrder _≡_etc. (decidable, ...)